Theorem vtoclbg 3520

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 3518	1 ⊢ (𝐴 ∈ 𝑉 → (𝜒 ↔ 𝜃))

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

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 2147

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

This theorem is used by:  alexeqg  3605  pm13.183  3620  elab6g  3623  elabgw  3631  sbc8g  3747  sbc2or  3748  sbccow  3762  sbcco  3765  sbc5ALT  3768  sbcie2g  3779  eqsbc1  3785  sbcng  3786  sbcimg  3787  sbcan  3788  sbcor  3789  sbcbig  3790  sbcal  3798  sbcex2  3799  sbcel1v  3804  sbcreu  3823  csbiebg  3879  sbcel12  4369  sbceqg  4370  csbie2df  4401  preq12bg  4813  elintrabg  4921  sbcbr123  5159  inisegn0  6096  fsn2g  7139  funfvima3  7242  elixpsn  8965  ixpsnf1o  8966  domeng  8989  elhf2g  9911  rankcf  10862  kardeng  35825  eldm3  36526  elima4  36540  brsset  36651  brbigcup  36660  elfix2  36666  elfunsg  36678  elsingles  36680  funpartlem  36706  ellines  36917  bj-elpwgALT  37969  cover2g  38650