Theorem vtoclbg 3526

Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 29-Apr-1994.)

Hypotheses

Ref	Expression
vtoclbg.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
vtoclbg.2	⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))
vtoclbg.3	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
vtoclbg	⊢ (𝐴 ∈ 𝑉 → (𝜒 ↔ 𝜃))

Distinct variable groups:   𝑥,𝐴   𝜒,𝑥   𝜃,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)   𝑉(𝑥)

Proof of Theorem vtoclbg

Step	Hyp	Ref	Expression
1		vtoclbg.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
2		vtoclbg.2	. . 3 ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))
3	1, 2	bibi12d 348	. 2 ⊢ (𝑥 = 𝐴 → ((𝜑 ↔ 𝜓) ↔ (𝜒 ↔ 𝜃)))
4		vtoclbg.3	. 2 ⊢ (𝜑 ↔ 𝜓)
5	3, 4	vtoclg 3524	1 ⊢ (𝐴 ∈ 𝑉 → (𝜒 ↔ 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2146

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-clel 2840

This theorem is used by:  alexeqg  3612  pm13.183  3627  elab6g  3630  elabgw  3638  sbc8g  3754  sbc2or  3755  sbccow  3769  sbcco  3772  sbc5ALT  3775  sbcie2g  3786  eqsbc1  3792  sbcng  3793  sbcimg  3794  sbcan  3795  sbcor  3796  sbcbig  3797  sbcal  3805  sbcex2  3806  sbcel1v  3811  sbcreu  3830  csbiebg  3886  sbcel12  4376  sbceqg  4377  csbie2df  4408  preq12bg  4820  elintrabg  4928  sbcbr123  5167  inisegn0  6102  fsn2g  7138  funfvima3  7241  elixpsn  8941  ixpsnf1o  8942  domeng  8965  rankcf  10779  kardeng  35629  eldm3  36292  elima4  36307  brsset  36418  brbigcup  36427  elfix2  36433  elfunsg  36445  elsingles  36447  funpartlem  36473  ellines  36683  elhf2g  36707  bj-elpwgALT  37749  cover2g  38427